\begin{tabbing}
$\forall$${\it es}$:ES, $a$:Atom1, $e$:E.
\\[0ex]$e$ sends $a$ $\vee$ (state when $e$):state@loc($e$)$>>$$a$
\\[0ex]$\Rightarrow$ \=loc($e$) $>>$ $a$\+
\\[0ex]$\vee$ ($\exists$${\it e'}$:E. ${\it e'}$ $\leq$ $e$  \& ${\it e'}$ receives $a$)
\\[0ex]$\vee$ (state when es{-}init(${\it es}$;$e$)):state@loc(es{-}init(${\it es}$;$e$))$>>$$a$
\-
\end{tabbing}